Lawrence C. Paulson; "A Mechanised Proof of Gödel’s Incompleteness Theorems using Nominal Isabelle"

Gödelの不完全性定理は遺伝的有限集合の集合論に基づいて証明可能である

という事実を用いて使っている

その他de Bruijnインデックスで論理式や構文を定めると簡潔になってよいということなどが書かれている

1章

執筆時当時

第1不完全性定理は3回定理証明支援系によって証明されている

Natarajan ShankarによるNqthmによる証明(1986)

Russell O’ConnorによるCoqの証明(2004)

HarrisonによるHOL Lightでの証明(2004)

上の証明ではde Bruijnインデックスによって煩雑さを避けており，この論文でもそれを採用する？

2章.1

マイルストーンをいくつか置く

1. 一階の演繹計算(deductive calculus)を形式化する．

演繹計算は

項と論理式の構文

代入

意味論（評価）

Peano算術あるいは，遺伝的有限集合論の公理を含む（今回は後者）

命題や量化子についての推論規則

公理の集合$ Hから$ Aが演繹計算によって証明されるとき$ H \vdash A

2, 真理と証明性についてのメタ定理をいくつか置く

演繹計算におけるあまりにも面倒な記述を避ける．

一つは，原子式と$ \lor,\land,\exists及び全称有界量化による$ \Sigma文について，

$ \alphaが真の$ \Sigma文$ \implies$ \vdash \alphaという結果を導く

3, Gödel数化が形式的な一階理論にあることを示す．

論理式$ \varphiのGödel数が$ \ulcorner\varphi\urcornerでり，その数項が導出可能

4. $ \vdash \varphi$ \iff$ \mathrm{Pf}(\ulcorner \varphi \urcorner)

$ \mathrm{Pf}(\ulcorner \varphi \urcorner)が$ \varphiが証明を持つということを表す論理式であるとする．

Gödelの第1不完全性定理は，論理式$ \deltaが証明不可能であるという形式的な記述と，演繹計算において等しい文$ \deltaを作ることで得られる

$ \deltaは意味論では死んであるのに$ \deltaもその否定も導出計算の中では証明できない，

次の補題を示す．

$ \alphaが$ \Sigma文$ \implies$ \vdash \alpha \to \mathrm{Pf}(\ulcorner\alpha\urcorner)

内面化補題と呼ばれる．

$ \Sigma文の構造についての帰納法で示せる．

2章.2

公理

1. $ z=0 \leftrightarrow \forall x \lbrack x \notin z \rbrack

2. $ z = x \triangleleft y \leftrightarrow \forall u \lbrack (u \in z) \leftrightarrow (u \in x \lor u = y\rbrack)

3. $ \varphi(0) \lor \forall x. \forall y. \lbrack \varphi(x) \land \forall\varphi(y) \rbrack